package interfaces.gestores;

import interfaces.ITecnico;
import tdg.contract.semanticAnnotations.ImportClass;
import tdg.contract.semanticAnnotations.Init;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Query;

@Init ({""})
@Inv ({""})

public interface IGestorTecnicos {
	
	@Pre ({"t!=null #NullPointerException"})
	public void bajaTecnico(ITecnico t);
	
	@Pre ({"tecnico!=null && nuevoTecnico != null #NullPointerException", "tecnico.getID() == nuevoTecnico.getID()"})
	public void modificarTecnico(ITecnico tecnico, ITecnico nuevoTecnico);
	
	@Pre ({"nuevoTecnico!=null #NullPointerException"})
	public void altaTecnico(ITecnico nuevoTecnico);
}
